Inference at * 2 2 1 
Iof proof for Lemma select nth tl:



1. T : Type
2. T List
3. u : T
4. v : T List
5. n:{0...||v||}, i:{0..(||v|| - n)}. nth_tl(n;v)[i] = v[(i+n)]
6. n : {0...||v||+1}
7. i : {0..((||v||+1) - n)}
8. 0 < n
  v[(i+(n - 1))] = [u / v][(i+n)] 

latex

 by ((RWO "select_cons_tl" 0) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n
C),(first_nat 3:n)) (first_tok SupInf:t) inil_term))) 

latex

C.

Definitions	, True, T, P & Q, P  Q, t  T, P  Q, P  Q, {i..j}, {i...j}, x:A. B(x)
Lemmas	le wf, squash wf, select cons tl, length wf1, select wf